00100	3. Integer Squareroot 
00200	
00300		The desired program should find         , the floor of the
00400	squareroot of its input x.  This task was chosen to coincide with
00500	Zohar Manna's tutorial on Automatic Programming [3rd IJCAI], which
00600	compared existing systems' abilities to synthesize or verify this
00700	code.  PUP's impressive performance was gained by sacrificing 
00800	formal methods -- and the associated formal guarantees.
00900	
01000		PUP is given just the right knowledge about numeric functions,
01100	number systems, ordering, maxima and minima, searching, and the real
01200	square root function to make the problem interesting yet doable.
01300	For example, PUP does not know any program to compute   x, given x.
01400	However, it does know how to test if an input is equal to   x, namely
01500	compute the square of that input.  PUP  __does__ have a program to
01600	compute square: (λ (y) (times y y)).  Let us investigate the
01700	dialog now.
01800	
01900		The user asks for ISQRT(82). Since PUP doesn't recognize
02000	ISQRT, it assumes the user either made a typo or is about to have
02100	PUP write a new function.  THe user settles that question, and 
02200	PUP notices that there is one argument, and it is numeric. The
02300	knowledge of numeric functions is sufficient to realize that the
02400	domain and range of the function should be pinpointed, if possible.
02500	In this case, the user must indicate that the range is integral.
02600	For example, he might type back that both domain and range are N,
02700	the set of natural numbers.  PUP now picks names for the input
02800	and output, say x and y, and asks the user to describe the function
02900	in terms of these variables. THe user replies
03000	MAX Y SUCH THAT   Y ≤ SQUAREROOT(X).
03100	
03200		At this stage, PUP worries about two semi-independent
03300	things. One is whether or not the condition following the SUCH THAT
03400	is testable -- i.e., does PUP have a program already which can do
03500	it.  As we mentioned earlier, we did not give PUP this much knowledge
03600	about real SQUAREROOT -- it has no algorithm to compute it.  THe
03700	second worry is whether an algorithm is known to compute the MAXimum
03800	element of the range satisfying a given test.  Since the range is
03900	the natural numbers, the answer to this is also negative.
04000	
04100		The first worry, in detail, is that y ≤ SQUAREROOT(X)
04200	might not be testable, given x and y.  Knowledge of the ≤ function
04300	says that we can do the test iff each side is computable. Of course
04400	we can compute y, given x and y. BUt we cannot find an algorithm
04500	to compute SQUAREROOT(x), so we must look deeper.  Knowledge of
04600	inequalities says that we may fix this up by finding an inverse
04700	function, I,  to SQUAREROOT,  replacing the old inequality by
04800	I(x) ≤ y.  A warning note says that such an I must be computable,
04900	(and in addition both I and SQUAREROOT must be monotone functions)
05000	else we're no better off than when we started.  By "luck," our
05100	main fact about squareroot is that its inverse function is SQUARE.
05200	Both SQUAREROOT and SQUARE have a tag indicating monotonicity. Also,
05300	SQUARE knows itself to be computable, so we now have the statement
05400	MAX Y SUCH THAT   SQUARE(Y) ≤ X.
     

00100		Our second worry was about an algorithm for finding
00200	MAX Y SUCH THAT   P(Y).   Knowledge about MAX says that the
00300	only algorithm it knows is to start by choosing Y as the upper
00400	bound of the range, then iterate, decrementing Y each time,
00500	until P is satisfied.  Knowledge of the natural numbers says
00600	that the upper bound does not exist, so the program
00700	(LAMBDA (X) (ISQRT1 (UPPERBOUND NATURAL_NUMBERS)  X))
00800	where we define the auxilliary function ISQRT1
00900	(LAMBDA (Y X) (COND   (P(Y)     Y)
01000			      (T       (ISQRT1   Y-1   X))))
01100	and where P(Y) would be replace by our now testable predicate
01200	(SQUARE Y) ≤ X,
01300	is impossible.   Fortunately, MAX knows a transformation of itself,
01400	if P is a monotone predicate and if the range is a segement of the
01500	integers. Namely,  MAX Y SUCH THAT P(Y)  becomes
01600	MIN Y SUCH THAT ¬P(Y+1).  Both the conditions are verified in our
01700	case, so we tentatively make the change and examine our algorithms
01800	for MIN.  The only one we have says to start at the lower bound of the
01900	range and repeatedly increment Y until the conditions are met.
02000	But natural number knowledge informs us that a lower bound is zero.
02100	So our expression now looks like this:
02200	MIN Y SUCH THAT  ¬(  (Y+1)   ≤ X). Notice that PUP implicitly assumes
02300	that NOT of a computable predicate is computable. This should be made
02400	explicit, probably. Rewriting all this into LISP, PUP arrives at:
02500	(LAMBDA(X) (ISQRT1 0 X)), where we again have an auxilliary function:
02600	(LAMBDA (Y X) (COND ((GREATERP (SQUARE (ADD1 Y)) X)     Y)
02700			    ( T			(ISQRT1 (ADD1 Y) X))))
02800	Knowledge of NOT let us replace NOT(≤ . .) by (> . .)  at this point.
02900	
03000		Now that PUP has written the program, it enters it in its
03100	records, recalls the original request, and runs the new program on
03200	it. While this is a "correct" program, it is fairly inefficient.
03300	Since Manna's lecture was to be on writing better squareroot code,
03400	Lenat added facilities for optimization: The recursion was replaced
03500	by an iteration, a new binary chop algorithm was provided, and
03600	information about algebraic expansion was furnished.  The binary
03700	chop demanded that the range be bounded above and below. So PUP had
03800	to figure out that the upper bound exisited after all: for any 
03900	natural number x, its squareroot is ≤ x, hence ISQRT(X) is bounded
04000	above by X.  With this alone, PUP could write the following:
04100	(LAMBDA (X) (PROG (Y Y2)
04200		(SETQ Y 0)
04300		(SETQ Y2 X)
04400	   L:	(COND ((GREATERP (SQUARE (HALF (PLUS Y Y2)))   X) 
04500		       (SETQ Y2 (HALF (PLUS Y Y2))))
04600		      (T (SETQ Y (HALF (PLUS Y Y2)))))
04700		(COND ((EQUAL Y Y2) (RETURN Y))
04800		      (T (GO L)))))
04900	Above, HALF refers to integer division by two, and is assumed to be
05000	known.  As a final touch, knowledge that (a + b)  = a  + 2ab + b
05100	can provide a basis for eliminating the costly SQUARE operation.
05200	Of course, it is amusing to worry about this level of efficiency
05300	in LISP, so we shall not pursue it further here.  Notice the flavor
05400	of this dialog in general, however:  locating relevant information,
05500	which in turn provides some of the final code and/or points to
05600	more information which is needed.  It is the sense of purpose which
05700	beats the combinatorial explosion of what to look at; it is the
05800	structuring of knowledge which beats the combinatorial explosion
05900	of locating relevant facts.  These ideas are carried further in
06000	the later PUP systems.